/**
Examples taken from the paper
"A Framework for the Flexible Integration of a Class of
Decision Procedures into Theorem Provers",
Predrag Janicic, Alan Bundy, Ian Green
*/

\problem {
	\forall int k; \forall int l;
	(0 < k & 0 < l & 2*k+1 < 2*l -> 2*k+2<=2*l)
}